es:event_system{i:l}, x:Id, T:Type, e:es-E(es).
es-dtype(es; loc(e); x; T)
 ((es-first(es; e)))
 (es-after(es; x; es-pred(es; e)) = es-when(es; x; e)  T) 

latex

Definitions	es-first(es; e), loc(e), b, <a, b>, es-after(es; x; e), es-when(es; x; e), es-vartype(es; i; x), x:A. B(x), x:AB(x), t  T, s = t, A, P  Q, es-dtype(es; i; x; T), P  Q, es-E(es), t.1, Type, Id, atom{$n:n}, event_system{i:l}, x:A  B(x), prop{i:l}
Lemmas	es-when wf, es-after-pred, event system wf, Id wf, es-E wf, es-loc wf, es-dtype wf, es-first wf, assert wf, not wf